Search Results

Documents authored by Parys, Pawel

Document
DOI: 10.4230/LIPIcs.FSCD.2018.27
Homogeneity Without Loss of Generality

Authors: Pawel Parys

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We consider higher-order recursion schemes as generators of infinite trees. A sort (simple type) is called homogeneous when all arguments of higher order are taken before any arguments of lower order. We prove that every scheme can be converted into an equivalent one (i.e, generating the same tree) that is homogeneous, that is, uses only homogeneous sorts. Then, we prove the same for safe schemes: every safe scheme can be converted into an equivalent safe homogeneous scheme. Furthermore, we compare two definition of safe schemes: the original definition of Damm, and the modern one. Finally, we prove a lemma which illustrates usefulness of the homogeneity assumption. The results are known, but we prove them in a novel way: by directly manipulating considered schemes.
Cite as

Pawel Parys. Homogeneity Without Loss of Generality. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.FSCD.2018.27,
  author =	{Parys, Pawel},
  title =	{{Homogeneity Without Loss of Generality}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.27},
  URN =		{urn:nbn:de:0030-drops-91972},
  doi =		{10.4230/LIPIcs.FSCD.2018.27},
  annote =	{Keywords: higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.53
Recursion Schemes and the WMSO+U Logic

Authors: Pawel Parys

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
We study the weak MSO logic extended by the unbounding quantifier (WMSO+U), expressing the fact that there exist arbitrarily large finite sets satisfying a given property. We prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+U.
Cite as

Pawel Parys. Recursion Schemes and the WMSO+U Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 53:1-53:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.STACS.2018.53,
  author =	{Parys, Pawel},
  title =	{{Recursion Schemes and the WMSO+U Logic}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{53:1--53:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.53},
  URN =		{urn:nbn:de:0030-drops-85122},
  doi =		{10.4230/LIPIcs.STACS.2018.53},
  annote =	{Keywords: higher-order recursion schemes, intersection types, WMSO+U logic, boundedness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.45
The Complexity of the Diagonal Problem for Recursion Schemes

Authors: Pawel Parys

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We consider nondeterministic higher-order recursion schemes as recognizers of languages of finite words or finite trees. We establish the complexity of the diagonal problem for schemes: given a set of letters A and a scheme G, is it the case that for every number n the scheme accepts a word (a tree) in which every letter from A appears at least n times. We prove that this problem is (m-1)-EXPTIME-complete for word-recognizing schemes of order m, and m-EXPTIME-complete for tree-recognizing schemes of order m.
Cite as

Pawel Parys. The Complexity of the Diagonal Problem for Recursion Schemes. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.FSTTCS.2017.45,
  author =	{Parys, Pawel},
  title =	{{The Complexity of the Diagonal Problem for Recursion Schemes}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.45},
  URN =		{urn:nbn:de:0030-drops-83757},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.45},
  annote =	{Keywords: diagonal problem, higher-order recursion schemes, intersection types, downward closure}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.11
Models of Lambda-Calculus and the Weak MSO Logic

Authors: Pawel Parys and Szymon Torunczyk

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
We study the weak MSO logic in relationship to infinitary lambda-calculus. We show that for every formula phi of weak MSO there exists a finitary model of infinitary lambda-calculus recognizing the set of infinitary lambda-terms whose Böhm tree satisfies phi. The model is effective, in the sense that for every lambda-Y-term we can effectively compute its value in the model. In particular, given a finite lambda-Y-term, one can decide whether the resulting Böhm tree satisfies a given formula of weak MSO, which is a special case of the result of Ong, which concerns unrestricted MSO. The existence of effective models for weak MSO and MSO was proved earlier by Salvati and Walukiewicz but our proof uses a different method, as it does not involve automata, but works directly with logics.
Cite as

Pawel Parys and Szymon Torunczyk. Models of Lambda-Calculus and the Weak MSO Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{parys_et_al:LIPIcs.CSL.2016.11,
  author =	{Parys, Pawel and Torunczyk, Szymon},
  title =	{{Models of Lambda-Calculus and the Weak MSO Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{11:1--11:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.11},
  URN =		{urn:nbn:de:0030-drops-65511},
  doi =		{10.4230/LIPIcs.CSL.2016.11},
  annote =	{Keywords: typed lambda-calculus, models, weak MSO logic}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.20
Reasoning About Integrity Constraints for Tree-Structured Data

Authors: Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
We study a class of integrity constraints for tree-structured data modelled as data trees, whose nodes have a label from a finite alphabet and store a data value from an infinite data domain. The constraints require each tuple of nodes selected by a conjunctive query (using navigational axes and labels) to satisfy a positive combination of equalities and a positive combination of inequalities over the stored data values. Such constraints are instances of the general framework of XML-to-relational constraints proposed recently by Niewerth and Schwentick. They cover some common classes of constraints, including W3C XML Schema key and unique constraints, as well as domain restrictions and denial constraints, but cannot express inclusion constraints, such as reference keys. Our main result is that consistency of such integrity constraints with respect to a given schema (modelled as a tree automaton) is decidable. An easy extension gives decidability for the entailment problem. Equivalently, we show that validity and containment of unions of conjunctive queries using navigational axes, labels, data equalities and inequalities is decidable, as long as none of the conjunctive queries uses both equalities and inequalities; without this restriction, both problems are known to be undecidable. In the context of XML data exchange, our result can be used to establish decidability for a consistency problem for XML schema mappings. All the decision procedures are doubly exponential, with matching lower bounds. The complexity may be lowered to singly exponential, when conjunctive queries are replaced by tree patterns, and the number of data comparisons is bounded.
Cite as

Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys. Reasoning About Integrity Constraints for Tree-Structured Data. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICDT.2016.20,
  author =	{Czerwinski, Wojciech and David, Claire and Murlak, Filip and Parys, Pawel},
  title =	{{Reasoning About Integrity Constraints for Tree-Structured Data}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.20},
  URN =		{urn:nbn:de:0030-drops-57897},
  doi =		{10.4230/LIPIcs.ICDT.2016.20},
  annote =	{Keywords: data trees, integrity constraints, unions of conjunctive queries, schema mappings, entailment, containment, consistency}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.19
On a Fragment of AMSO and Tiling Systems

Authors: Achim Blumensath, Thomas Colcombet, and Pawel Parys

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We prove that satisfiability over infinite words is decidable for a fragment of asymptotic monadic second-order logic. In this fragment we only allow formulae of the form "exists t forall s exists r: phi(r,s,t)", where phi does not use quantifiers over number variables, and variables r and s can be only used simultaneously, in subformulae of the form s < f(x) <= r.
Cite as

Achim Blumensath, Thomas Colcombet, and Pawel Parys. On a Fragment of AMSO and Tiling Systems. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{blumensath_et_al:LIPIcs.STACS.2016.19,
  author =	{Blumensath, Achim and Colcombet, Thomas and Parys, Pawel},
  title =	{{On a Fragment of AMSO and Tiling Systems}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.19},
  URN =		{urn:nbn:de:0030-drops-57202},
  doi =		{10.4230/LIPIcs.STACS.2016.19},
  annote =	{Keywords: monadic second-order logic, boundedness, tiling problems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.21
The MSO+U Theory of (N,<) Is Undecidable

Authors: Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.
Cite as

Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2016.21,
  author =	{Bojanczyk, Mikolaj and Parys, Pawel and Torunczyk, Szymon},
  title =	{{The MSO+U Theory of (N,\langle) Is Undecidable}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{21:1--21:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.21},
  URN =		{urn:nbn:de:0030-drops-57223},
  doi =		{10.4230/LIPIcs.STACS.2016.21},
  annote =	{Keywords: automata, logic, unbounding quantifier, bounds, undecidability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.163
Ordered Tree-Pushdown Systems

Authors: Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.
Cite as

Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered Tree-Pushdown Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 163-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.FSTTCS.2015.163,
  author =	{Clemente, Lorenzo and Parys, Pawel and Salvati, Sylvain and Walukiewicz, Igor},
  title =	{{Ordered Tree-Pushdown Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{163--177},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.163},
  URN =		{urn:nbn:de:0030-drops-56470},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.163},
  annote =	{Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.99
Decidable classes of documents for XPath

Authors: Vince Bárány, Mikolaj Bojanczyk, Diego Figueira, and Pawel Parys

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
We study the satisfiability problem for XPath over XML documents of bounded depth. We define two parameters, called match width and braid width, that assign a number to any class of documents. We show that for all k, satisfiability for XPath restricted to bounded depth documents with match width at most k is decidable; and that XPath is undecidable on any class of documents with unbounded braid width. We conjecture that these two parameters are equivalent, in the sense that a class of documents has bounded match width iff it has bounded braid width.
Cite as

Vince Bárány, Mikolaj Bojanczyk, Diego Figueira, and Pawel Parys. Decidable classes of documents for XPath. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 99-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{barany_et_al:LIPIcs.FSTTCS.2012.99,
  author =	{B\'{a}r\'{a}ny, Vince and Bojanczyk, Mikolaj and Figueira, Diego and Parys, Pawel},
  title =	{{Decidable classes of documents for XPath}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{99--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.99},
  URN =		{urn:nbn:de:0030-drops-38512},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.99},
  annote =	{Keywords: XPath, XML, class automata, data trees, data words, satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.500
Variants of Collapsible Pushdown Systems

Authors: Pawel Parys

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We analyze the relationship between three ways of generating trees using collapsible pushdown systems (CPS's): using deterministic CPS's, nondeterministic CPS's, and deterministic word-accepting CPS's. We prove that (for each level of the CPS and each input alphabet) the three classes of trees are equal. The nontrivial translations increase n-1 times exponentially the size of the level-n CPS. The same results stay true if we restrict ourselves to higher-order pushdown systems without collapse. As a second contribution we prove that the hierarchy of word languages recognized by nondeterministic CPS's is infinite. This is a consequence of a lemma which bounds the length of the shortest accepting run. It also implies that the hierarchy of epsilon-closures of configuration graphs is infinite (which was already known). As a side effect we obtain a new algorithm for the reachability problem for CPS's; it has the same complexity as previously known algorithms.
Cite as

Pawel Parys. Variants of Collapsible Pushdown Systems. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 500-515, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.CSL.2012.500,
  author =	{Parys, Pawel},
  title =	{{Variants of Collapsible Pushdown Systems}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{500--515},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.500},
  URN =		{urn:nbn:de:0030-drops-36937},
  doi =		{10.4230/LIPIcs.CSL.2012.500},
  annote =	{Keywords: collapsible pushdown systems, determinization, infinite hierarchy, shrink- ing lemma, reachability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.54
A Pumping Lemma for Pushdown Graphs of Any Level

Authors: Pawel Parys

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
We present a pumping lemma for the class of epsilon-contractions of pushdown graphs of level n, for each n. A pumping lemma was proposed by Blumensath, but there is an irrecoverable error in his proof; we present a new proof. Our pumping lemma also improves the bounds given in the invalid paper of Blumensath.
Cite as

Pawel Parys. A Pumping Lemma for Pushdown Graphs of Any Level. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 54-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.STACS.2012.54,
  author =	{Parys, Pawel},
  title =	{{A Pumping Lemma for Pushdown Graphs of Any Level}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{54--65},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.54},
  URN =		{urn:nbn:de:0030-drops-33940},
  doi =		{10.4230/LIPIcs.STACS.2012.54},
  annote =	{Keywords: pushdown graph, epsilon-contraction, pumping lemma}
}
Document
DOI: 10.4230/LIPIcs.STACS.2011.603
Collapse Operation Increases Expressive Power of Deterministic Higher Order Pushdown Automata

Authors: Pawel Parys

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Abstract
We show that collapsible deterministic second level pushdown automata can recognize more languages than deterministic second level pushdown automata (without collapse). This implies that there exists a tree generated by a second level recursion scheme which is not generated by any second level safe recursion scheme.
Cite as

Pawel Parys. Collapse Operation Increases Expressive Power of Deterministic Higher Order Pushdown Automata. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 603-614, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.STACS.2011.603,
  author =	{Parys, Pawel},
  title =	{{Collapse Operation Increases Expressive Power of Deterministic Higher Order Pushdown Automata}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{603--614},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.603},
  URN =		{urn:nbn:de:0030-drops-30478},
  doi =		{10.4230/LIPIcs.STACS.2011.603},
  annote =	{Keywords: pushdown automata}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact